形式手法 検証アプローチ
検証アプローチは主に
形式仕様記述
モデル検査
定理証明支援系
がある。
プログラム検証というものもあるっぽい。定理証明を包括するものがプログラム検証というものになる。
定理証明$ \subset プログラム検証
(形式手法の導入PDFより)
アプローチ方法は以下がある
モデルベースアプローチ
(VDM, Z, B)
代数アプローチ
(Act One, Larch, OBJ)
プロセス代数
(CSP(形式手法), CCS)
論理アプローチ
(RTL, TLA)
リアクティブアプローチ
(Petri-­‐nets, SDL, SAO)
複合アプローチ
RAISE (VDM + CSP)
LOTOS(Act One + CCS)
参考
2012/11/15
成功した形式手法導入調査例の分析と発見